﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.FOL.Logic;
using TruthTree2.FOL.Resolution;

namespace TruthTree2.FOL.ResolutionExtensions
{
    public static class ResolutionExtensions
    {
        #region eliminateConditionals
        internal static WFF eliminateConditionals(this WFF f)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is ComplexWFF) { return eliminateConditionals((ComplexWFF)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF eliminateConditionals(this ComplexWFF f)
        {
            if (f is Connective) { return eliminateConditionals((Connective)f); }
            else if (f is Quantifier) { return eliminateConditionals((Quantifier)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF eliminateConditionals(this Quantifier q)
        {
            if (q is Existential) { return new Existential(q.variable, eliminateConditionals(q.scope)); }
            else if (q is Universal) { return new Universal(q.variable, eliminateConditionals(q.scope)); }

            throw new NotImplementedException(q.GetType().ToString());
        }

        internal static WFF eliminateConditionals(this Connective c)
        {
            if (c is Biconditional) { return eliminateConditionals((Biconditional)c); }
            else if (c is Conditional) { return eliminateConditionals((Conditional)c); }
            else if (c is Conjunction) { return eliminateConditionals((Conjunction)c); }
            else if (c is Disjunction) { return eliminateConditionals((Disjunction)c); }
            else if (c is Negation) { return eliminateConditionals((Negation)c); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        internal static WFF eliminateConditionals(this Biconditional b)
        {
            Disjunction left = new Disjunction(
                b.left.GetNegation(),
                b.right);
            Disjunction right = new Disjunction(
                b.right.GetNegation(),
                b.left);

            return new Conjunction(
                eliminateConditionals(left),
                eliminateConditionals(right));
        }

        internal static WFF eliminateConditionals(this Conditional c)
        {
            return new Disjunction(
                eliminateConditionals(c.antecedent).GetNegation(),
                eliminateConditionals(c.consequent));
        }

        internal static WFF eliminateConditionals(this Conjunction c)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = eliminateConditionals(c.conjuncts[a]);
            }

            return new Conjunction(cons);
        }

        internal static WFF eliminateConditionals(this Disjunction d)
        {
            WFF[] diss = new WFF[d.disjuncts.Length];
            for (int a = 0; a < diss.Length; a++)
            {
                diss[a] = eliminateConditionals(d.disjuncts[a]);
            }

            return new Disjunction(diss);
        }

        internal static WFF eliminateConditionals(this Negation n)
        {
            return new Negation(eliminateConditionals(n.inner));
        }
        #endregion

        #region moveNotsInwards
        internal static WFF moveNotsInwards(this WFF f)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is ComplexWFF) { return moveNotsInwards((ComplexWFF)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF moveNotsInwards(this ComplexWFF f)
        {
            if (f is Connective) { return moveNotsInwards((Connective)f); }
            else if (f is Quantifier) { return moveNotsInwards((Quantifier)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF moveNotsInwards(this Quantifier q)
        {
            if (q is Existential) { return new Existential(q.variable, moveNotsInwards(q.scope)); }
            else if (q is Universal) { return new Universal(q.variable, moveNotsInwards(q.scope)); }

            throw new NotImplementedException(q.GetType().ToString());
        }

        internal static WFF moveNotsInwards(this Connective c)
        {
            if (c is Conjunction) { return moveNotsInwards((Conjunction)c); }
            else if (c is Disjunction) { return moveNotsInwards((Disjunction)c); }
            else if (c is Negation) { return moveNotsInwards((Negation)c); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        internal static WFF moveNotsInwards(this Conjunction c)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = moveNotsInwards(c.conjuncts[a]);
            }

            return new Conjunction(cons);
        }

        internal static WFF moveNotsInwards(this Disjunction d)
        {
            WFF[] diss = new WFF[d.disjuncts.Length];
            for (int a = 0; a < diss.Length; a++)
            {
                diss[a] = moveNotsInwards(d.disjuncts[a]);
            }

            return new Disjunction(diss);
        }

        internal static WFF moveNotsInwards(this Negation n)
        {
            if (n.inner is Conjunction)
            {
                Conjunction inner = (Conjunction)n.inner;
                WFF[] cons = new WFF[inner.conjuncts.Length];
                for (int a = 0; a < cons.Length; a++)
                {
                    cons[a] = moveNotsInwards(inner.conjuncts[a].GetNegation());
                }

                return new Disjunction(cons);
            }
            else if (n.inner is Disjunction)
            {
                Disjunction inner = (Disjunction)n.inner;
                WFF[] diss = new WFF[inner.disjuncts.Length];
                for (int a = 0; a < diss.Length; a++)
                {
                    diss[a] = moveNotsInwards(inner.disjuncts[a].GetNegation());
                }

                return new Conjunction(diss);
            }
            else if (n.inner is Existential)
            {
                Existential inner = (Existential)n.inner;
                return new Universal(
                    inner.variable,
                    moveNotsInwards(inner.scope.GetNegation()));
            }
            else if (n.inner is Negation)
            {
                Negation inner = (Negation)n.inner;
                return inner.inner;
            }
            else if (n.inner is Universal)
            {
                Universal inner = (Universal)n.inner;
                return new Existential(
                    inner.variable,
                    moveNotsInwards(inner.scope.GetNegation()));
            }

            return n;
        }
        #endregion

        #region standardize
        internal static WFF standardize(this WFF f)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is ComplexWFF) { return standardize((ComplexWFF)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF standardize(this ComplexWFF f)
        {
            if (f is Connective) { return standardize((Connective)f); }
            else if (f is Quantifier) { return standardize((Quantifier)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF standardize(this Quantifier q)
        {
            if (q is Existential)
            {
                UniqueVariable u = new UniqueVariable();
                return new Existential(
                    u,
                    standardize(q.scope.Rename(q.variable, u)));
            }
            else if (q is Universal)
            {
                UniqueVariable u = new UniqueVariable();
                return new Universal(
                    u,
                    standardize(q.scope.Rename(q.variable, u)));
            }

            throw new NotImplementedException(q.GetType().ToString());
        }

        internal static WFF standardize(this Connective c)
        {
            if (c is Conjunction) { return standardize((Conjunction)c); }
            else if (c is Disjunction) { return standardize((Disjunction)c); }
            else if (c is Negation) { return standardize((Negation)c); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        internal static WFF standardize(this Conjunction c)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = standardize(c.conjuncts[a]);
            }

            return new Conjunction(cons);
        }

        internal static WFF standardize(this Disjunction d)
        {
            WFF[] diss = new WFF[d.disjuncts.Length];
            for (int a = 0; a < diss.Length; a++)
            {
                diss[a] = standardize(d.disjuncts[a]);
            }

            return new Disjunction(diss);
        }

        internal static WFF standardize(this Negation n)
        {
            return new Negation(standardize(n.inner));
        }
        #endregion

        #region skolemize
        private static WFF skolemize(this WFF f, HashSet<Variable> bound)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is ComplexWFF) { return skolemize((ComplexWFF)f, bound); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        private static WFF skolemize(this ComplexWFF f, HashSet<Variable> bound)
        {
            if (f is Connective) { return skolemize((Connective)f, bound); }
            else if (f is Quantifier) { return skolemize((Quantifier)f, bound); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        private static WFF skolemize(this Quantifier q, HashSet<Variable> bound)
        {
            if (q is Existential)
            {
                SkolemFunction fn = new SkolemFunction(bound.ToArray());
                return skolemize(q.scope.Rename(q.variable, fn), bound);
            }
            else if (q is Universal)
            {
                HashSet<Variable> nbound = new HashSet<Variable>(bound);
                nbound.Add(q.variable);
                return new Universal(
                    q.variable,
                    skolemize(q.scope, nbound));
            }

            throw new NotImplementedException(q.GetType().ToString());
        }

        private static WFF skolemize(this Connective c, HashSet<Variable> bound)
        {
            if (c is Conjunction) { return skolemize((Conjunction)c, bound); }
            else if (c is Disjunction) { return skolemize((Disjunction)c, bound); }
            else if (c is Negation) { return skolemize((Negation)c, bound); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        private static WFF skolemize(this Conjunction c, HashSet<Variable> bound)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = skolemize(c.conjuncts[a], bound);
            }

            return new Conjunction(cons);
        }

        private static WFF skolemize(this Disjunction d, HashSet<Variable> bound)
        {
            WFF[] diss = new WFF[d.disjuncts.Length];
            for (int a = 0; a < diss.Length; a++)
            {
                diss[a] = skolemize(d.disjuncts[a], bound);
            }

            return new Disjunction(diss);
        }

        private static WFF skolemize(this Negation n, HashSet<Variable> bound)
        {
            return new Negation(skolemize(n.inner, bound));
        }
        #endregion

        internal static WFF skolemizeFormula(this WFF f)
        {
            HashSet<Variable> bound = new HashSet<Variable>();
            return skolemize(f, bound);
        }

        #region dropQuantifiers
        internal static WFF dropQuantifiers(this WFF f)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is ComplexWFF) { return dropQuantifiers((ComplexWFF)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF dropQuantifiers(this ComplexWFF f)
        {
            if (f is Connective) { return dropQuantifiers((Connective)f); }
            else if (f is Quantifier) { return dropQuantifiers((Quantifier)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF dropQuantifiers(this Quantifier q)
        {
            if (q is Universal)
            {
                return dropQuantifiers(q.scope);
            }

            throw new NotImplementedException(q.GetType().ToString());
        }

        internal static WFF dropQuantifiers(this Connective c)
        {
            if (c is Conjunction) { return dropQuantifiers((Conjunction)c); }
            else if (c is Disjunction) { return dropQuantifiers((Disjunction)c); }
            else if (c is Negation) { return dropQuantifiers((Negation)c); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        internal static WFF dropQuantifiers(this Conjunction c)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = dropQuantifiers(c.conjuncts[a]);
            }

            return new Conjunction(cons);
        }

        internal static WFF dropQuantifiers(this Disjunction d)
        {
            WFF[] diss = new WFF[d.disjuncts.Length];
            for (int a = 0; a < diss.Length; a++)
            {
                diss[a] = dropQuantifiers(d.disjuncts[a]);
            }

            return new Disjunction(diss);
        }

        internal static WFF dropQuantifiers(this Negation n)
        {
            return new Negation(dropQuantifiers(n.inner));
        }
        #endregion

        #region distributeOrs
        internal static WFF distributeOrs(this WFF f)
        {
            if (f is AtomicWFF) { return f; }
            else if (f is Connective) { return distributeOrs((Connective)f); }

            throw new NotImplementedException(f.GetType().ToString());
        }

        internal static WFF distributeOrs(this Connective c)
        {
            if (c is Conjunction) { return distributeOrs((Conjunction)c); }
            else if (c is Disjunction) { return distributeOrs((Disjunction)c); }
            else if (c is Negation) { return distributeOrs((Negation)c); }

            throw new NotImplementedException(c.GetType().ToString());
        }

        internal static WFF distributeOrs(this Conjunction c)
        {
            WFF[] cons = new WFF[c.conjuncts.Length];
            for (int a = 0; a < cons.Length; a++)
            {
                cons[a] = distributeOrs(c.conjuncts[a]);
            }

            return new Conjunction(cons);
        }

        internal static WFF distributeOrs(this Disjunction d)
        {
            // Disjunction of 0 or 1 things?
            if (d.disjuncts.Length < 2)
            {
                if (d.disjuncts.Length == 0) { return new Disjunction(); } // Weird stuff
                else { return distributeOrs(d.disjuncts[0]); }
            }

            // Magic here
            Conjunction c = (Conjunction)d.disjuncts.FirstOrDefault(f => { return f is Conjunction; });
            if (c == null) { return d; }

            List<WFF> others = new List<WFF>();
            foreach (WFF a in d.disjuncts)
            {
                if (a.Equals(c)) { continue; }
                others.Add(a);
            }

            List<WFF> disjunctions = new List<WFF>();
            foreach (WFF a in c.conjuncts)
            {
                List<WFF> diss = new List<WFF>(others);
                diss.Add(a);
                disjunctions.Add(distributeOrs(new Disjunction(diss.ToArray())));
            }

            return new Conjunction(disjunctions.ToArray());
        }

        internal static WFF distributeOrs(this Negation n)
        {
            return new Negation(distributeOrs(n.inner));
        }
        #endregion

        public static WFF ConvertToCNF(this WFF f)
        {
            WFF eliminated = f.eliminateConditionals();
            WFF moved = eliminated.moveNotsInwards();
            WFF standardized = moved.standardize();
            WFF skolemized = standardized.skolemizeFormula();
            WFF dropped = skolemized.dropQuantifiers();
            WFF distributed = dropped.distributeOrs();

            return distributed;
        }
    }
}
